(* $Id: xCoreInternals.mli 74 2007-10-16 12:20:18Z yann.regisgianas $ *)

(* Pangolin, a functional programming language for correct programs.
   Copyright (C) 2007, Yann Régis-Gianas, François Pottier.
   Contact: yann.regisgianas@gmail.com

   This program is free software: you can redistribute it and/or modify
   it under the terms of the GNU General Public License as published by
   the Free Software Foundation, either version 3 of the License, or
   any later version.

   This program is distributed in the hope that it will be useful,
   but WITHOUT ANY WARRANTY; without even the implied warranty of
   MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
   GNU General Public License for more details.

   You should have received a copy of the GNU General Public License
   along with this program.  If not, see <http://www.gnu.org/licenses/>. *)

(** FIXME *)
type t = MultiEquation.crterm

(** FIXME *)
val fresh :
  MultiEquation.variable_kind -> PIdentifier.t -> MultiEquation.variable

(** FIXME *)
val fresh_constant : string -> MultiEquation.variable

(** FIXME *)
val fresh_from_atom :
  MultiEquation.variable_kind -> XCoreSyntax.Var.Atom.t -> MultiEquation.variable

(** FIXME *)
type env = (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list

(** FIXME *)
val empty_env : 'a list

(** FIXME *)
val introduce_type_variable :
  MultiEquation.variable_kind ->
  'a ->
  PIdentifier.t ->
  ('a * MultiEquation.variable) list -> ('a * MultiEquation.variable) list

(** FIXME *)
val lookup_type_variable : XCoreSyntax.Var.Atom.t -> (XCoreSyntax.Var.Atom.t * 'a) list -> 'a

(** FIXME *)
val internal_prop_constant : MultiEquation.variable

(** FIXME *)
val internal_product_constant : MultiEquation.variable

(** FIXME *)
val internal_arrow_constant : MultiEquation.variable

(** FIXME *)
val internal_larrow_constant : MultiEquation.variable

(** FIXME *)
val internal_int_constant : MultiEquation.variable

(** FIXME *)
val internal_bool_constant : MultiEquation.variable

(** FIXME *)
val internal_unit_constant : MultiEquation.variable

(** FIXME *)
val internal_primitive_constants :
  (MultiEquation.variable * XCoreSyntax.Raw.primitive_type) list

(** FIXME *)
val internal_formula_primitive_constants :
  (MultiEquation.variable * XCoreSyntax.Raw.formula_type) list

(** FIXME *)
val internal_primitive_constants_variables : MultiEquation.variable list

(** FIXME *)
exception NotPrimitive

(** FIXME *)
val as_primitive : MultiEquation.variable -> XCoreSyntax.Raw.primitive_type

(** FIXME *)
val as_formula_primitive : MultiEquation.variable -> XCoreSyntax.Raw.formula_type

(** FIXME *)
val is_arrow : MultiEquation.variable -> bool

(** FIXME *)
val is_larrow : MultiEquation.variable -> bool

(** FIXME *)
val is_prod : MultiEquation.variable -> bool

(** FIXME *)
val internalize_app_type :
  'a -> 'a CoreAlgebra.arterm list -> 'a CoreAlgebra.arterm

(** FIXME *)
val unapp :
  MultiEquation.structure ->
  MultiEquation.variable * MultiEquation.variable list

(** FIXME *)
val mk_binop :
  'a ->
  'a CoreAlgebra.arterm -> 'a CoreAlgebra.arterm -> 'a CoreAlgebra.arterm

(** FIXME *)
val mk_arrow :
  MultiEquation.variable CoreAlgebra.arterm ->
  MultiEquation.variable CoreAlgebra.arterm ->
  MultiEquation.variable CoreAlgebra.arterm

(** FIXME *)
val mk_larrow :
  MultiEquation.variable CoreAlgebra.arterm ->
  MultiEquation.variable CoreAlgebra.arterm ->
  MultiEquation.variable CoreAlgebra.arterm

(** FIXME *)
val mk_prod :
  MultiEquation.variable CoreAlgebra.arterm list ->
  MultiEquation.variable CoreAlgebra.arterm

(** FIXME *)
val mk_n_arrow :
  MultiEquation.variable CoreAlgebra.arterm list ->
  MultiEquation.variable CoreAlgebra.arterm ->
  MultiEquation.variable CoreAlgebra.arterm

(** FIXME *)
val mk_n_larrow :
  MultiEquation.variable CoreAlgebra.arterm list ->
  MultiEquation.variable CoreAlgebra.arterm ->
  MultiEquation.variable CoreAlgebra.arterm

(** FIXME *)
val internalize_primitive_type :
  XCoreSyntax.primitive_type -> MultiEquation.variable CoreAlgebra.arterm

(** FIXME *)
val internalize_term_type :
  (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list ->
  XCoreSyntax.term_type -> MultiEquation.variable CoreAlgebra.arterm

(** FIXME *)
val introduce_type_variable_from_atom :
  MultiEquation.variable_kind ->
  XCoreSyntax.Var.Atom.t ->
  (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list ->
  (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list

(** FIXME *)
val introduce_rigid_type_variables :
  (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list ->
  XCoreSyntax.Var.Atom.t list ->
  (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list

(** FIXME *)
val introduce_flexible_type_variables :
  (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list ->
  XCoreSyntax.Var.Atom.t list ->
  (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list

(** FIXME *)
val link : MultiEquation.crterm -> MultiEquation.variable

(** FIXME *)
val internalize_type_scheme :
  (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list ->
  XCoreSyntax.type_scheme ->
  (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list * XCoreSyntax.type_parameters *
  MultiEquation.variable

(** FIXME *)
val internalize_formula_type :
  (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list ->
  XCoreSyntax.formula_type -> MultiEquation.variable CoreAlgebra.arterm

(** FIXME *)
val internalize_formula_type_scheme :
  (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list ->
  XCoreSyntax.formula_type_scheme ->
  (XCoreSyntax.Var.Atom.t * MultiEquation.variable) list * XCoreSyntax.type_parameters *
  MultiEquation.variable

(** FIXME *)
val name_from_int : int -> string

(** FIXME *)
val gi : int ref

(** FIXME *)
val ghistory : (MultiEquation.variable * XCoreSyntax.Raw.var) list ref

(** FIXME *)
val lhistory : XCoreSyntax.Raw.type_parameters ref

(** FIXME *)
val reset : unit -> unit

(** FIXME *)
val local_var : bool -> XCoreSyntax.Raw.type_parameter -> unit

(** FIXME *)
val new_name : bool -> MultiEquation.variable -> XCoreSyntax.Raw.var

(** FIXME *)
val type_scheme : int -> MultiEquation.variable -> XCoreSyntax.Raw.type_scheme

(** FIXME *)
val term_type' : int -> MultiEquation.crterm -> XCoreSyntax.Raw.term_type

(** FIXME *)
val term_type : int -> MultiEquation.variable -> XCoreSyntax.Raw.term_type

(** FIXME *)
val formula_type_scheme :
  int -> MultiEquation.variable -> XCoreSyntax.Raw.formula_type_scheme

(** FIXME *)
val rigid_var :
  MultiEquation.descriptor -> int -> MultiEquation.variable -> XCoreSyntax.Raw.formula_type

(** FIXME *)
val flexible_var :
  MultiEquation.descriptor -> int -> MultiEquation.variable -> XCoreSyntax.Raw.formula_type

(** FIXME *)
val var : int -> MultiEquation.variable -> XCoreSyntax.Raw.formula_type

(** FIXME *)
val term : int -> MultiEquation.structure -> XCoreSyntax.Raw.formula_type

(** FIXME *)
val formula_type : int -> MultiEquation.variable -> XCoreSyntax.Raw.formula_type

(** FIXME *)
val formula_type' : int -> MultiEquation.crterm -> XCoreSyntax.Raw.formula_type
